ltg:(IdLnkIdType), i:Id, k:Knd, T:Type.
(ltg  da-outlinks(k : T;i))
 {isrcv(k) & source(lnk(k)) = i
 {& (1of(ltg) ~ lnk(k))
 {& (1of(2of(ltg)) ~ tag(k))
 {& 2of(2of(ltg)) = T} 

latex

Definitions	A, (x  l), IdLnk, Id, x : v, da-outlinks(da;i), da-outlink-f(da;k), has-src(i;k), fpf-dom-list(f), mapfilter(f;P;L), P  Q, Knd, f(x), isrcv(k), lnk(k), tag(k), P  Q, a = b, , b, source(l), False, P  Q, P & Q, True, SQType(T), P  Q, {T}, 1of(t), Prop, t  T, 2of(t), x. t(x), x:A. B(x)
Lemmas	pi2 wf, Id wf, pi1 wf, IdLnk wf, Id sq, IdLnk sq, member singleton, lsrc wf, assert wf, bool wf, eq id wf, eqff to assert, bool sq, assert-eq-id, eqtt to assert, iff transitivity, bool cases, false wf, l member wf, nil member, not functionality wrt iff, Knd wf, fpf-single wf, da-outlinks wf